Nuprl Lemma : imin_add_r 13,42
a, b, c:. imin(a;b)+c = imin(a+c;b+c) 
latex

Upint 2, int 2
Definitions, t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, True, T
Lemmasimin wf, minus mono wrt eq, minus imin, add functionality wrt eq, add com, imax wf, true wf, squash wf, imax add r

origin